package autoz.czt.test;

import java.util.ArrayList;
import java.util.List;

import net.sourceforge.czt.base.ast.Term;
import net.sourceforge.czt.parser.util.CztError;
import net.sourceforge.czt.parser.util.ParseException;
import net.sourceforge.czt.session.CommandException;
import net.sourceforge.czt.session.FileSource;
import net.sourceforge.czt.session.Key;
import net.sourceforge.czt.session.Markup;
import net.sourceforge.czt.session.SectionManager;
import net.sourceforge.czt.session.Source;
import net.sourceforge.czt.typecheck.z.ErrorAnn;
import net.sourceforge.czt.typecheck.z.TypeChecker;
import net.sourceforge.czt.typecheck.z.impl.Factory;
import net.sourceforge.czt.z.ast.Spec;
import net.sourceforge.czt.z.ast.ZFactory;
import net.sourceforge.czt.z.impl.ZFactoryImpl;

public class CZTCommunication {
	
	public static void main(String[] args) throws CommandException{
		String file = "/local/d0p6/jw/Projects/autoz/autoz.czt/tex/simple.tex";
		CZTCommunication.testCommWithCZT(file);
	}
	
	public static void testCommWithCZT(String file) throws CommandException{
		List<? extends ErrorAnn> errors = new ArrayList<ErrorAnn>();
		Spec spec = null;
		
		SectionManager manager = new SectionManager();
		spec = parse(file, manager);
		
		try{
			ParseException parseException = (ParseException)manager.get(new Key<ParseException>(file, ParseException.class));
			if (parseException != null){
				System.out.println("Parse errors:");
				for (CztError e : parseException.getErrors()){
					System.out.println(e);
				}
			}
		} catch (CommandException e){
			throw e;
		}
		
		if (spec!= null){
			errors = typecheck(spec, manager);

			if (errors.size() > 0){
				System.out.println("Typecheck errors:");
				for (ErrorAnn ae : errors){
					System.out.println(ae);
				}
			} else{
				System.out.println("No errors found.");
			}
		}
	}
	
	private static Spec parse(String file, SectionManager manager) throws CommandException{
		Source source = new FileSource(file);
		source.setMarkup(Markup.LATEX);

		manager.put(new Key<Source>(file, Source.class), source);
		
		return manager.get(new Key<Spec>(file, Spec.class));
	}
	
	private static List<? extends ErrorAnn> typecheck(Term term, SectionManager manager){
		ZFactory zFactory = new ZFactoryImpl();
		TypeChecker typeChecker = new TypeChecker(new Factory(zFactory), manager, false);
		
		typeChecker.setUseNameIds(false);
		term.accept(typeChecker);
		
		return typeChecker.errors();
	}
}
